[Merged by Bors] - chore: fix diamonds around R and C structures by sgouezel · Pull Request #38451 · leanprover-community/mathlib4

sgouezel · 2026-04-24T09:18:28Z

The following examples fail on master, work with the PR:

example : (Semiring.toNatAlgebra : Algebra ℕ ℂ) = Complex.instAlgebraOfReal := by
  with_reducible_and_instances rfl

example : (Ring.toIntAlgebra ℂ : Algebra ℤ ℂ) = Complex.instAlgebraOfReal := by
  with_reducible_and_instances rfl

example : Module.restrictScalars ℝ ℂ ℂ = Complex.instModule := by
  with_reducible_and_instances rfl

example : (instInnerProductSpaceRealComplex.toSMul : SMul ℝ ℂ) = Complex.instRCLike.toSMul := by
  with_reducible_and_instances rfl

example {F : Type*} [NormedAddCommGroup F] [NormedSpace ℂ F] : SMulCommClass ℂ ℝ F :=
  inferInstance

The PR makes a few algebra maps implicit-reducible. This is necessary to get rid of the diamonds as these maps show up in the instances. This has no noticeable performance impact: implicit-reducible only matters for instances, and there it tends to help unification.

mathlib-bors · 2026-04-24T09:18:39Z

This pull request is now in draft mode. No active bors state needed cleanup.

While this PR remains draft, bors will ignore commands on this PR. Mark it ready for review before using commands like bors r+ or bors try.

github-actions · 2026-04-24T09:19:31Z

PR summary 5b5173e00f

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ ofFun

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

No changes to technical debt.

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

sgouezel · 2026-04-24T09:43:12Z

!radar

leanprover-radar · 2026-04-24T09:43:57Z

Benchmark results for 3c79bc9 against 79540a7 are in. There are significant results. @sgouezel

✅ build//instructions: -135.5G (-0.08%)

Large changes (1✅)

✅ build/module/Mathlib.Algebra.Category.CommAlgCat.Monoidal//instructions: -83.0G (-33.10%)

Medium changes (2✅)

✅ build/module/Mathlib.Algebra.Category.BialgCat.Monoidal//instructions: -11.5G (-17.62%)
✅ build/module/Mathlib.AlgebraicGeometry.GammaSpecAdjunction//instructions: -5.7G (-5.78%)

Small changes (10✅, 2🟥)

🟥 build/module/Mathlib.Algebra.Ring.TransferInstance//instructions: +253.0M (+2.43%)
✅ build/module/Mathlib.AlgebraicGeometry.SpreadingOut//instructions: -609.4M (-2.19%)
✅ build/module/Mathlib.AlgebraicGeometry.ValuativeCriterion//instructions: -699.9M (-2.90%)
🟥 build/module/Mathlib.Data.Matrix.Auto//instructions: +131.3M (+3.53%)
✅ build/module/Mathlib.FieldTheory.CardinalEmb//instructions: -2.2G (-1.81%)
✅ build/module/Mathlib.FieldTheory.Extension//instructions: -2.3G (-2.98%)
✅ build/module/Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits//instructions: -916.0M (-3.41%)
✅ build/module/Mathlib.RingTheory.Bialgebra.Hom//instructions: -889.5M (-3.17%)
✅ build/module/Mathlib.RingTheory.Etale.QuasiFinite//instructions: -9.5G (-3.29%)
✅ build/module/Mathlib.RingTheory.GradedAlgebra.AlgHom//instructions: -949.4M (-3.24%)
✅ build/module/Mathlib.RingTheory.TensorProduct.Maps//instructions: -9.0G (-4.62%)
✅ build/module/Mathlib.RingTheory.WittVector.IsPoly//instructions: -651.2M (-2.36%)

mathlib-merge-conflicts · 2026-04-25T03:47:34Z

This pull request has conflicts, please merge master and resolve them.

sgouezel · 2026-04-30T08:22:17Z

!radar

leanprover-radar · 2026-04-30T08:22:46Z

Benchmark results for eae998b against 5b5173e are in. There are significant results. @sgouezel

🟥 main exited with code 1

No significant changes detected.

sgouezel · 2026-04-30T09:33:50Z

!radar

leanprover-radar · 2026-04-30T09:34:16Z

Benchmark results for dc8867d against 5b5173e are in. No significant results found. @sgouezel

✅ build//instructions: -25.6G (-0.01%)

Small changes (6✅, 1🟥)

✅ build/module/Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order//instructions: -2.2G (-1.46%)
✅ build/module/Mathlib.Analysis.Complex.Harmonic.Analytic//instructions: -563.5M (-2.11%)
✅ build/module/Mathlib.Analysis.Distribution.TemperedDistribution//instructions: -3.0G (-2.78%)
✅ build/module/Mathlib.NumberTheory.ModularForms.Basic//instructions: -1.0G (-2.58%)
✅ build/module/Mathlib.NumberTheory.ModularForms.CuspFormSubmodule//instructions: -210.9M (-1.63%)
🟥 build/module/Mathlib.Util.AliasIn//instructions: +105.5M (+3.41%) (reduced significance based on absolute threshold)
✅ build/module/Mathlib.Util.TransImports//instructions: -93.0M (-3.41%)

kim-em · 2026-04-30T22:47:04Z

bors d+

mathlib-bors · 2026-04-30T22:47:07Z

✌️ sgouezel can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

This one is fixing a diamond which can not be encountered on master, but shows up after the fixes in #38451 (and fixing this diamond is necessary for #38451 to go through). The diamond is the following. If a space E is a C-module, then it is automatically an R-module (Module.complexToReal). Define now a type synonym E' to E, and declare that, if k acts on E, then it also acts on E', through `inferInstanceAs`. Then E' is a C-module (instance applied to k=C), and therefore an R-module by Module.complexToReal. But, as E is an R-module (by Module.complexToReal), then E' is also an R-module (by the instance applied to k=R). The two R-module structures are not the same implicit-reducibly, as the latter is hidden behind an opaque function crafted by `inferInstanceAs`. To avoid this, we define the `smul` field by hand instead of hiding it behind an opaque function. This should probably be done throughout Mathlib whenever a type synonym can be endowed with real and complex module structures. I'm just fixing one example here, because it's the one that breaks in #38451. Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

mathlib-dependent-issues · 2026-04-30T23:33:42Z

This PR/issue depends on:

~~[Merged by Bors] - chore: make .id and .comp implicit-reducible #38618~~
~~[Merged by Bors] - chore: export algebraMap from Algebra instead of having a def #38430~~
~~[Merged by Bors] - chore: fix implicit-reducible diamond in uniform convergence #38481~~
By Dependent Issues (🤖). Happy coding!

sgouezel · 2026-05-01T06:46:47Z

bors r+

The following examples fail on master, work with the PR: ```lean example : (Semiring.toNatAlgebra : Algebra ℕ ℂ) = Complex.instAlgebraOfReal := by with_reducible_and_instances rfl example : (Ring.toIntAlgebra ℂ : Algebra ℤ ℂ) = Complex.instAlgebraOfReal := by with_reducible_and_instances rfl example : Module.restrictScalars ℝ ℂ ℂ = Complex.instModule := by with_reducible_and_instances rfl example : (instInnerProductSpaceRealComplex.toSMul : SMul ℝ ℂ) = Complex.instRCLike.toSMul := by with_reducible_and_instances rfl example {F : Type*} [NormedAddCommGroup F] [NormedSpace ℂ F] : SMulCommClass ℂ ℝ F := inferInstance ``` The PR makes a few algebra maps implicit-reducible. This is necessary to get rid of the diamonds as these maps show up in the instances. This has no noticeable performance impact: implicit-reducible only matters for instances, and there it tends to help unification. Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

mathlib-bors · 2026-05-01T07:35:11Z

Pull request successfully merged into master.

Build succeeded:

sgouezel added 5 commits April 20, 2026 22:55

try

64837c4

test

ade3c75

fix

877f827

fix

1d5c768

try

3c79bc9

sgouezel marked this pull request as draft April 24, 2026 09:18

sgouezel added 3 commits April 24, 2026 13:17

fix

def8c1a

Merge branch 'SG_alge' into SG_red2

03388c2

better

160d127

sgouezel marked this pull request as ready for review April 24, 2026 12:54

mathlib-dependent-issues Bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Apr 24, 2026

matthewjasper mentioned this pull request Apr 24, 2026

chore: fix diamonds for Real/Complex Algebra instances #36087

Closed

1 task

sgouezel added 3 commits April 24, 2026 15:50

fix

c7fddc2

try real fix

a5dcfce

fix

d808645

j-loreaux reviewed Apr 24, 2026

View reviewed changes

Comment thread Mathlib/Algebra/Algebra/Pi.lean Outdated

This was referenced Apr 24, 2026

chore: make RingHom.comp implicit_reducible #38315

Closed

[Merged by Bors] - chore: fix implicit-reducible diamond in uniform convergence #38481

Closed

mathlib-merge-conflicts Bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Apr 25, 2026

merge master

0c62c1f

github-actions Bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Apr 25, 2026

merge master

eae998b

fix

dc8867d

mathlib-triage Bot added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Apr 30, 2026

mathlib-dependent-issues Bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Apr 30, 2026

mathlib-triage Bot added the ready-to-merge This PR has been sent to bors. label May 1, 2026

mathlib-bors Bot changed the title ~~chore: fix diamonds around R and C structures~~ [Merged by Bors] - chore: fix diamonds around R and C structures May 1, 2026

mathlib-bors Bot closed this May 1, 2026

Conversation

sgouezel commented Apr 24, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

mathlib-bors Bot commented Apr 24, 2026

Uh oh!

github-actions Bot commented Apr 24, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 5b5173e00f

Import changes for modified files

Declarations diff

Uh oh!

sgouezel commented Apr 24, 2026

Uh oh!

leanprover-radar commented Apr 24, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

mathlib-merge-conflicts Bot commented Apr 25, 2026

Uh oh!

sgouezel commented Apr 30, 2026

Uh oh!

leanprover-radar commented Apr 30, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

sgouezel commented Apr 30, 2026

Uh oh!

leanprover-radar commented Apr 30, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

kim-em commented Apr 30, 2026

Uh oh!

mathlib-bors Bot commented Apr 30, 2026

Uh oh!

mathlib-dependent-issues Bot commented Apr 30, 2026

Uh oh!

sgouezel commented May 1, 2026

Uh oh!

mathlib-bors Bot commented May 1, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

sgouezel commented Apr 24, 2026 •

edited

Loading

github-actions Bot commented Apr 24, 2026 •

edited

Loading

leanprover-radar commented Apr 24, 2026 •

edited

Loading

leanprover-radar commented Apr 30, 2026 •

edited

Loading

leanprover-radar commented Apr 30, 2026 •

edited

Loading